(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun r () Real)
(declare-fun s () Real)
(push)
(assert (= 1 (* i (to_int s))))
(check-sat)
(pop)
(assert (is_int (- s)))
(check-sat)
(assert (<= 0 (+ j 1)))
(assert (< j (* 3 (to_int r))))
(check-sat)
